$\forall$$A$:Type, $P$, $Q$:(($A$ List)$\rightarrow$Prop).
\\[0ex]safety($A$;$x$.$P$($x$))
\\[0ex]$\Rightarrow$ ($\forall$${\it tr}_{1}$, ${\it tr}_{2}$:$A$ List. ${\it tr}_{1}$ $\leq$ ${\it tr}_{2}$ $\Rightarrow$ $P$(${\it tr}_{2}$) $\Rightarrow$ $Q$(${\it tr}_{2}$) $\Rightarrow$ $Q$(${\it tr}_{1}$))
\\[0ex]$\Rightarrow$ safety($A$;$x$.$P$($x$) \& $Q$($x$))